WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {cons/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          append#(l1,l2) -> c_1(append#1#(l1,l2))
          append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
          append#1#(nil(),l2) -> c_3()
          subtrees#(t) -> c_4(subtrees#1#(t))
          subtrees#1#(leaf()) -> c_5()
          subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
          subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
          subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_1(append#1#(l1,l2))
            append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
            append#1#(nil(),l2) -> c_3()
            subtrees#(t) -> c_4(subtrees#1#(t))
            subtrees#1#(leaf()) -> c_5()
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
            subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/2,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {3,5}
        by application of
          Pre({3,5}) = {1,4}.
        Here rules are labelled as follows:
          1: append#(l1,l2) -> c_1(append#1#(l1,l2))
          2: append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
          3: append#1#(nil(),l2) -> c_3()
          4: subtrees#(t) -> c_4(subtrees#1#(t))
          5: subtrees#1#(leaf()) -> c_5()
          6: subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
          7: subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
          8: subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_1(append#1#(l1,l2))
            append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
            subtrees#(t) -> c_4(subtrees#1#(t))
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
            subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        - Weak DPs:
            append#1#(nil(),l2) -> c_3()
            subtrees#1#(leaf()) -> c_5()
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/2,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:append#(l1,l2) -> c_1(append#1#(l1,l2))
             -->_1 append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2)):2
             -->_1 append#1#(nil(),l2) -> c_3():7
          
          2:S:append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
             -->_1 append#(l1,l2) -> c_1(append#1#(l1,l2)):1
          
          3:S:subtrees#(t) -> c_4(subtrees#1#(t))
             -->_1 subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1)):4
             -->_1 subtrees#1#(leaf()) -> c_5():8
          
          4:S:subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
             -->_1 subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2)):5
             -->_2 subtrees#(t) -> c_4(subtrees#1#(t)):3
          
          5:S:subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
             -->_1 subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2)):6
             -->_2 subtrees#(t) -> c_4(subtrees#1#(t)):3
          
          6:S:subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
             -->_1 append#(l1,l2) -> c_1(append#1#(l1,l2)):1
          
          7:W:append#1#(nil(),l2) -> c_3()
             
          
          8:W:subtrees#1#(leaf()) -> c_5()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          8: subtrees#1#(leaf()) -> c_5()
          7: append#1#(nil(),l2) -> c_3()
* Step 4: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_1(append#1#(l1,l2))
            append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
            subtrees#(t) -> c_4(subtrees#1#(t))
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
            subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/2,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          subtrees#(t) -> c_4(subtrees#1#(t))
          subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
          subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
        and a lower component
          append#(l1,l2) -> c_1(append#1#(l1,l2))
          append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
          subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        Further, following extension rules are added to the lower component.
          subtrees#(t) -> subtrees#1#(t)
          subtrees#1#(node(x,t1,t2)) -> subtrees#(t1)
          subtrees#1#(node(x,t1,t2)) -> subtrees#2#(subtrees(t1),t1,t2,x)
          subtrees#2#(l1,t1,t2,x) -> subtrees#(t2)
          subtrees#2#(l1,t1,t2,x) -> subtrees#3#(subtrees(t2),l1,t1,t2,x)
** Step 4.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            subtrees#(t) -> c_4(subtrees#1#(t))
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/2,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:subtrees#(t) -> c_4(subtrees#1#(t))
             -->_1 subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1)):2
          
          2:S:subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
             -->_1 subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2)):3
             -->_2 subtrees#(t) -> c_4(subtrees#1#(t)):1
          
          3:S:subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#3#(subtrees(t2),l1,t1,t2,x),subtrees#(t2))
             -->_2 subtrees#(t) -> c_4(subtrees#1#(t)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#(t2))
** Step 4.a:2: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            subtrees#(t) -> c_4(subtrees#1#(t))
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#(t2))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/1,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          append :: ["A"(0) x "A"(2)] -(0)-> "A"(2)
          append#1 :: ["A"(0) x "A"(2)] -(0)-> "A"(2)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(2)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(4)
          leaf :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(5)
          node :: ["A"(0) x "A"(15) x "A"(15)] -(15)-> "A"(15)
          node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees :: ["A"(0)] -(0)-> "A"(2)
          subtrees#1 :: ["A"(0)] -(0)-> "A"(2)
          subtrees#2 :: ["A"(2) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(2)
          subtrees#3 :: ["A"(2) x "A"(2) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(3)
          subtrees# :: ["A"(15)] -(8)-> "A"(8)
          subtrees#1# :: ["A"(15)] -(1)-> "A"(12)
          subtrees#2# :: ["A"(0) x "A"(0) x "A"(15) x "A"(0)] -(8)-> "A"(5)
          c_4 :: ["A"(0)] -(0)-> "A"(12)
          c_6 :: ["A"(0) x "A"(0)] -(0)-> "A"(15)
          c_7 :: ["A"(7)] -(0)-> "A"(7)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_4_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "c_7_A" :: ["A"(0)] -(0)-> "A"(1)
          "cons_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "leaf_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "node_A" :: ["A"(0) x "A"(1) x "A"(1)] -(1)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          subtrees#(t) -> c_4(subtrees#1#(t))
        2. Weak:
          subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
          subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#(t2))
** Step 4.a:3: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#(t2))
        - Weak DPs:
            subtrees#(t) -> c_4(subtrees#1#(t))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/1,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          append :: ["A"(0) x "A"(3)] -(0)-> "A"(3)
          append#1 :: ["A"(0) x "A"(3)] -(0)-> "A"(3)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(15)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(14)
          leaf :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(13)
          node :: ["A"(12) x "A"(12) x "A"(12)] -(12)-> "A"(12)
          node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees :: ["A"(0)] -(0)-> "A"(5)
          subtrees#1 :: ["A"(0)] -(0)-> "A"(7)
          subtrees#2 :: ["A"(2) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(8)
          subtrees#3 :: ["A"(3) x "A"(1) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(9)
          subtrees# :: ["A"(12)] -(2)-> "A"(1)
          subtrees#1# :: ["A"(12)] -(2)-> "A"(1)
          subtrees#2# :: ["A"(3) x "A"(0) x "A"(12) x "A"(2)] -(3)-> "A"(12)
          c_4 :: ["A"(0)] -(0)-> "A"(12)
          c_6 :: ["A"(0) x "A"(0)] -(1)-> "A"(1)
          c_7 :: ["A"(0)] -(0)-> "A"(12)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_4_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(1)
          "c_7_A" :: ["A"(0)] -(0)-> "A"(1)
          "cons_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "leaf_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#(t2))
        2. Weak:
          subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
** Step 4.a:4: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
        - Weak DPs:
            subtrees#(t) -> c_4(subtrees#1#(t))
            subtrees#2#(l1,t1,t2,x) -> c_7(subtrees#(t2))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/1,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          append :: ["A"(0) x "A"(5)] -(0)-> "A"(3)
          append#1 :: ["A"(0) x "A"(5)] -(0)-> "A"(5)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(15)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(8)
          leaf :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(11)
          node :: ["A"(0) x "A"(12) x "A"(12)] -(12)-> "A"(12)
          node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees :: ["A"(0)] -(0)-> "A"(5)
          subtrees#1 :: ["A"(0)] -(0)-> "A"(5)
          subtrees#2 :: ["A"(5) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(5)
          subtrees#3 :: ["A"(5) x "A"(1) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(5)
          subtrees# :: ["A"(12)] -(5)-> "A"(12)
          subtrees#1# :: ["A"(12)] -(5)-> "A"(1)
          subtrees#2# :: ["A"(3) x "A"(0) x "A"(12) x "A"(0)] -(6)-> "A"(12)
          c_4 :: ["A"(0)] -(0)-> "A"(15)
          c_6 :: ["A"(0) x "A"(0)] -(0)-> "A"(11)
          c_7 :: ["A"(0)] -(0)-> "A"(15)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_4_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_6_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "c_7_A" :: ["A"(0)] -(0)-> "A"(1)
          "cons_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
          "leaf_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "node_A" :: ["A"(0) x "A"(1) x "A"(1)] -(1)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          subtrees#1#(node(x,t1,t2)) -> c_6(subtrees#2#(subtrees(t1),t1,t2,x),subtrees#(t1))
        2. Weak:
          

** Step 4.b:1: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_1(append#1#(l1,l2))
            append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
            subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        - Weak DPs:
            subtrees#(t) -> subtrees#1#(t)
            subtrees#1#(node(x,t1,t2)) -> subtrees#(t1)
            subtrees#1#(node(x,t1,t2)) -> subtrees#2#(subtrees(t1),t1,t2,x)
            subtrees#2#(l1,t1,t2,x) -> subtrees#(t2)
            subtrees#2#(l1,t1,t2,x) -> subtrees#3#(subtrees(t2),l1,t1,t2,x)
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/2,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          append :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          append#1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          leaf :: [] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(0)
          node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees :: ["A"(0)] -(0)-> "A"(0)
          subtrees#1 :: ["A"(0)] -(0)-> "A"(0)
          subtrees#2 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees#3 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          append# :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          append#1# :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees# :: ["A"(0)] -(1)-> "A"(0)
          subtrees#1# :: ["A"(0)] -(1)-> "A"(0)
          subtrees#2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0)
          subtrees#3# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(0)
          c_2 :: ["A"(0)] -(0)-> "A"(0)
          c_8 :: ["A"(0)] -(0)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
        
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        2. Weak:
          append#(l1,l2) -> c_1(append#1#(l1,l2))
          append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
** Step 4.b:2: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_1(append#1#(l1,l2))
            append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
        - Weak DPs:
            subtrees#(t) -> subtrees#1#(t)
            subtrees#1#(node(x,t1,t2)) -> subtrees#(t1)
            subtrees#1#(node(x,t1,t2)) -> subtrees#2#(subtrees(t1),t1,t2,x)
            subtrees#2#(l1,t1,t2,x) -> subtrees#(t2)
            subtrees#2#(l1,t1,t2,x) -> subtrees#3#(subtrees(t2),l1,t1,t2,x)
            subtrees#3#(l2,l1,t1,t2,x) -> c_8(append#(l1,l2))
        - Weak TRS:
            append(l1,l2) -> append#1(l1,l2)
            append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
            append#1(nil(),l2) -> l2
            subtrees(t) -> subtrees#1(t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(x,t1,t2)) -> subtrees#2(subtrees(t1),t1,t2,x)
            subtrees#2(l1,t1,t2,x) -> subtrees#3(subtrees(t2),l1,t1,t2,x)
            subtrees#3(l2,l1,t1,t2,x) -> cons(node(x,t1,t2),append(l1,l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5,append#/2,append#1#/2,subtrees#/1
            ,subtrees#1#/1,subtrees#2#/4,subtrees#3#/5} / {cons/2,leaf/0,nil/0,node/3,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0
            ,c_6/2,c_7/2,c_8/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,append#1#,subtrees#,subtrees#1#,subtrees#2#
            ,subtrees#3#} and constructors {cons,leaf,nil,node}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          append :: ["A"(12) x "A"(12)] -(0)-> "A"(12)
          append#1 :: ["A"(12) x "A"(12)] -(0)-> "A"(12)
          cons :: ["A"(0) x "A"(9)] -(9)-> "A"(9)
          cons :: ["A"(0) x "A"(12)] -(12)-> "A"(12)
          leaf :: [] -(0)-> "A"(15)
          nil :: [] -(0)-> "A"(12)
          nil :: [] -(0)-> "A"(14)
          node :: ["A"(15) x "A"(15) x "A"(15)] -(15)-> "A"(15)
          node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          subtrees :: ["A"(15)] -(1)-> "A"(12)
          subtrees#1 :: ["A"(15)] -(1)-> "A"(12)
          subtrees#2 :: ["A"(12) x "A"(0) x "A"(15) x "A"(0)] -(13)-> "A"(12)
          subtrees#3 :: ["A"(12) x "A"(12) x "A"(0) x "A"(0) x "A"(0)] -(12)-> "A"(12)
          append# :: ["A"(9) x "A"(0)] -(2)-> "A"(14)
          append#1# :: ["A"(9) x "A"(0)] -(1)-> "A"(14)
          subtrees# :: ["A"(15)] -(14)-> "A"(0)
          subtrees#1# :: ["A"(15)] -(2)-> "A"(0)
          subtrees#2# :: ["A"(12) x "A"(0) x "A"(15) x "A"(0)] -(14)-> "A"(0)
          subtrees#3# :: ["A"(12) x "A"(11) x "A"(0) x "A"(0) x "A"(0)] -(4)-> "A"(12)
          c_1 :: ["A"(0)] -(0)-> "A"(14)
          c_2 :: ["A"(0)] -(0)-> "A"(14)
          c_8 :: ["A"(0)] -(0)-> "A"(14)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_2_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_8_A" :: ["A"(0)] -(0)-> "A"(1)
          "cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "leaf_A" :: [] -(0)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
          "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          append#(l1,l2) -> c_1(append#1#(l1,l2))
          append#1#(cons(x,xs),l2) -> c_2(append#(xs,l2))
        2. Weak:
          

WORST_CASE(?,O(n^2))